\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $l$:IdLnk, ${\it tgs}$:(Id List), ${\it ks}$:(Knd List),\+
\\[0ex]$g$:(\=$k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$)\} $\rightarrow$(${\it tg}$:\{${\it tg}$:Id$\mid$ (${\it tg}$ $\in$ ${\it tgs}$)\} \+
\\[0ex]$\times$ \=(decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$\+
\\[0ex](fpf{-}cap(${\it da}$; Kind{-}deq; rcv($l$,${\it tg}$); void) List))) List).
\-\-\-\\[0ex]no\_repeats(Id; ${\it tgs}$)
\\[0ex]$\Rightarrow$ l\_all(${\it tgs}$; Id; ${\it tg}$.($\uparrow$fpf{-}dom(Kind{-}deq; rcv($l$,${\it tg}$); ${\it da}$)))
\\[0ex]$\Rightarrow$ \=($\forall$${\it es}$:event\_system\{i:l\}. \+
\\[0ex](l\_all(\=${\it ks}$;\+
\\[0ex]Knd;
\\[0ex]$k$.sends{-}p(${\it es}$; ${\it ds}$; $k$; fpf{-}cap(${\it da}$; Kind{-}deq; $k$; void); $l$; es{-}dt($l$; ${\it da}$); ($g$($k$))))
\-\\[0ex]$\wedge$ l\_all(${\it tgs}$; Id; ${\it tg}$.sframe{-}p(${\it es}$; $l$; ${\it tg}$; ${\it ks}$)))
\\[0ex]$\Rightarrow$ es{-}decls(${\it es}$;source($l$);${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ \=with decls \=${\it ds}$ \+\+
\\[0ex]${\it da}$
\-\\[0ex]sends on $l$ from $e$ 
\\[0ex]include \=if deq{-}member(Kind{-}deq; es{-}kind(${\it es}$; $e$); ${\it ks}$)\+
\\[0ex]then tagged{-}list{-}messages(\=es{-}state{-}when(${\it es}$; $e$);\+
\\[0ex]es{-}val(${\it es}$; $e$);
\\[0ex]($g$(es{-}kind(${\it es}$; $e$))))
\-\\[0ex]else []
\\[0ex]fi  
\-\\[0ex]and only these for tags in ${\it tgs}$)
\-\-
\end{tabbing}